(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 2))
(declare-fun v1 () (_ BitVec 5))
(declare-fun v2 () (_ BitVec 7))
(declare-fun v3 () (_ BitVec 11))
(assert (let ((e4(_ bv100 8)))
(let ((e5(_ bv47 6)))
(let ((e6 (bvshl v2 v2)))
(let ((e7 (bvurem e6 e6)))
(let ((e8 (bvmul v3 ((_ zero_extend 3) e4))))
(let ((e9 (ite (= (_ bv1 1) ((_ extract 6 6) e7)) ((_ zero_extend 4) v2) e8)))
(let ((e10 (ite (distinct v3 e9) (_ bv1 1) (_ bv0 1))))
(let ((e11 (bvsrem ((_ zero_extend 1) e5) v2)))
(let ((e12 (ite (bvsge e4 ((_ zero_extend 7) e10)) (_ bv1 1) (_ bv0 1))))
(let ((e13 (bvsrem ((_ sign_extend 4) v2) e9)))
(let ((e14 (bvxnor v3 e9)))
(let ((e15 (bvadd e9 ((_ zero_extend 4) e6))))
(let ((e16 (ite (= (_ bv1 1) ((_ extract 0 0) e10)) ((_ sign_extend 1) v2) e4)))
(let ((e17 (bvadd e8 e15)))
(let ((e18 (bvashr ((_ sign_extend 1) e5) v2)))
(let ((e19 (bvsub ((_ zero_extend 10) e10) e17)))
(let ((e20 (ite (bvslt e6 ((_ sign_extend 5) v0)) (_ bv1 1) (_ bv0 1))))
(let ((e21 (bvadd ((_ zero_extend 3) e16) e8)))
(let ((e22 (bvxor e4 e16)))
(let ((e23 (bvneg e4)))
(let ((e24 (ite (bvule e14 ((_ zero_extend 4) v2)) (_ bv1 1) (_ bv0 1))))
(let ((e25 (ite (bvsge ((_ zero_extend 5) e5) e8) (_ bv1 1) (_ bv0 1))))
(let ((e26 (bvlshr ((_ sign_extend 3) v1) e23)))
(let ((e27 (distinct e17 ((_ zero_extend 4) e11))))
(let ((e28 (bvuge e17 v3)))
(let ((e29 (bvslt ((_ zero_extend 4) e7) e13)))
(let ((e30 (bvugt e21 e19)))
(let ((e31 (bvule e14 ((_ zero_extend 6) v1))))
(let ((e32 (distinct e8 ((_ zero_extend 4) e6))))
(let ((e33 (bvsge e23 ((_ sign_extend 1) e7))))
(let ((e34 (bvugt ((_ sign_extend 7) e25) e23)))
(let ((e35 (bvule v2 v2)))
(let ((e36 (bvugt ((_ zero_extend 1) e18) e26)))
(let ((e37 (bvslt e13 e14)))
(let ((e38 (bvugt e15 e17)))
(let ((e39 (bvuge e16 ((_ zero_extend 3) v1))))
(let ((e40 (distinct e17 e14)))
(let ((e41 (bvugt e17 v3)))
(let ((e42 (= e14 ((_ zero_extend 4) e11))))
(let ((e43 (bvult ((_ zero_extend 6) e12) e7)))
(let ((e44 (bvsle ((_ sign_extend 3) e22) e8)))
(let ((e45 (bvule e14 ((_ sign_extend 9) v0))))
(let ((e46 (bvslt e14 ((_ zero_extend 10) e25))))
(let ((e47 (bvugt e26 ((_ sign_extend 1) e7))))
(let ((e48 (bvule e7 ((_ sign_extend 6) e24))))
(let ((e49 (bvsge e14 ((_ zero_extend 3) e22))))
(let ((e50 (bvule e18 ((_ zero_extend 6) e25))))
(let ((e51 (bvsge ((_ sign_extend 6) e12) v2)))
(let ((e52 (bvsge e11 ((_ zero_extend 6) e10))))
(let ((e53 (bvsgt ((_ zero_extend 6) v1) e8)))
(let ((e54 (bvult v3 e8)))
(let ((e55 (bvuge e14 e14)))
(let ((e56 (distinct e16 ((_ zero_extend 7) e20))))
(let ((e57 (bvsgt ((_ zero_extend 10) e24) v3)))
(let ((e58 (= e17 ((_ zero_extend 4) e11))))
(let ((e59 (bvult ((_ sign_extend 3) e22) e9)))
(let ((e60 (bvule e15 ((_ sign_extend 5) e5))))
(let ((e61 (bvslt e15 ((_ zero_extend 3) e16))))
(let ((e62 (bvuge v3 e19)))
(let ((e63 (bvugt ((_ zero_extend 1) e6) e22)))
(let ((e64 (bvult ((_ zero_extend 3) e23) e13)))
(let ((e65 (bvuge ((_ sign_extend 4) e18) e19)))
(let ((e66 (bvult ((_ zero_extend 10) e12) e9)))
(let ((e67 (bvult ((_ zero_extend 6) e20) e6)))
(let ((e68 (bvslt e13 ((_ sign_extend 5) e5))))
(let ((e69 (bvsle ((_ zero_extend 10) e25) e17)))
(let ((e70 (bvsgt ((_ sign_extend 10) e25) e14)))
(let ((e71 (bvsle e19 e14)))
(let ((e72 (bvsge ((_ sign_extend 9) v0) e17)))
(let ((e73 (bvsle ((_ sign_extend 5) e5) v3)))
(let ((e74 (bvugt e13 ((_ sign_extend 9) v0))))
(let ((e75 (bvugt e4 ((_ sign_extend 6) v0))))
(let ((e76 (not e46)))
(let ((e77 (or e60 e56)))
(let ((e78 (ite e52 e44 e72)))
(let ((e79 (ite e64 e70 e45)))
(let ((e80 (=> e50 e47)))
(let ((e81 (xor e65 e57)))
(let ((e82 (=> e62 e74)))
(let ((e83 (xor e38 e28)))
(let ((e84 (xor e83 e43)))
(let ((e85 (and e76 e39)))
(let ((e86 (ite e77 e30 e78)))
(let ((e87 (=> e86 e33)))
(let ((e88 (ite e55 e68 e61)))
(let ((e89 (=> e36 e58)))
(let ((e90 (=> e69 e79)))
(let ((e91 (and e41 e32)))
(let ((e92 (or e35 e73)))
(let ((e93 (xor e89 e81)))
(let ((e94 (ite e93 e71 e34)))
(let ((e95 (or e91 e87)))
(let ((e96 (ite e84 e95 e94)))
(let ((e97 (not e51)))
(let ((e98 (not e96)))
(let ((e99 (or e31 e75)))
(let ((e100 (=> e85 e49)))
(let ((e101 (or e67 e27)))
(let ((e102 (and e88 e100)))
(let ((e103 (=> e59 e40)))
(let ((e104 (= e63 e101)))
(let ((e105 (= e37 e42)))
(let ((e106 (=> e54 e53)))
(let ((e107 (=> e29 e105)))
(let ((e108 (xor e107 e98)))
(let ((e109 (or e99 e97)))
(let ((e110 (and e90 e80)))
(let ((e111 (ite e48 e92 e92)))
(let ((e112 (and e108 e102)))
(let ((e113 (and e66 e104)))
(let ((e114 (xor e82 e112)))
(let ((e115 (not e103)))
(let ((e116 (or e111 e110)))
(let ((e117 (and e109 e115)))
(let ((e118 (or e116 e106)))
(let ((e119 (and e117 e118)))
(let ((e120 (or e119 e114)))
(let ((e121 (and e120 e113)))
(let ((e122 (and e121 (not (= v2 (_ bv0 7))))))
(let ((e123 (and e122 (not (= v2 (bvnot (_ bv0 7)))))))
(let ((e124 (and e123 (not (= e9 (_ bv0 11))))))
(let ((e125 (and e124 (not (= e9 (bvnot (_ bv0 11)))))))
(let ((e126 (and e125 (not (= e6 (_ bv0 7))))))
e126
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
